$\forall$$A$:Type\{i\}, $r$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$\{i\}). WellFnd\{i\}($A$;$x$,$y$.$r$($x$,$y$)) $\in$ $\mathbb{P}$\{i'\}